Inhalt des Dokuments

Bachelor

Formalisierung der Verifikation eines Konsens-Algorithmus mit Isabelle

Samstag, 09. Juni 2012

Betreuer/in: Küfner
Erstgutachter/in: Prof. Dr.-Ing. Nestmann
Zweitgutachter/in: Dr. Kammüller

Rickmann, Christina

In Isabelle wurde ein weit verbreiteter Consensus-Algorithmus formal verifiziert. Die Verifkation der geforderten Safety-Eigenschaften dieses Algorithmus wurde auf Basis eines inkrementellen Invariantenstils durchgeführt.  Die Aufgabe besteht nun darin die Eigenschaften erneut jedoch entlang eines vorliegenden Papierbeweises nachzuweisen und Vor-und Nachteile der beiden Beweisarten zu vergleichen.

---